1. Field of the Invention
The invention relates generally to design of digital systems, e.g., a computer or a component of a computer. More specifically, the invention relates to a method and apparatus for constructing a latch mapping.
2. Background Art
Modern computer and electrical engineers use hardware description languages such as Verilog HDL and VHDL to describe a digital system from a functional specification of the digital system. The engineers may describe the digital system at different levels of abstraction. One of the higher-level descriptions of the digital system is the register transfer level (RTL). In the RTL, variables and data operators are used to describe registers and transfer of vectors of information between registers. For example, in the RTL, a very simple digital circuit performing an AND operation may be described as xe2x80x9cOUT=aandb,xe2x80x9d where xe2x80x9candxe2x80x9d represents the AND operation between the variables a and b and OUT represents the output of the digital circuit. The next lower-level description of the digital system is the gate level. At the gate level, the digital system may be described as a set of interconnected logic gates, e.g., AND and OR, and memory components, e.g., flip-flops and latches. FIG. 1 shows a gate level description 2 of the RTL description: xe2x80x9cOUT=aandb.xe2x80x9d The lowest-level description of the digital system is the transistor level. At the transistor level, the digital system may be described as a set of interconnected wires, resistors, and transistors on an integrated circuit (IC) chip. The transistor-level schematic is used to create the physical model of the IC chip. FIG. 2 shows the digital circuit of FIG. 1 at the transistor level. The digital circuit includes two transistors 4, 6 which are coupled to perform an AND operation on input signals a and b.
In practice, a digital system would consist of hundreds of thousands to millions of transistors. Thus, formal verification is important in designing functionally correct digital systems. Formal verification is checking to see whether the system performs its intended function. One form of formal verification called equivalence checking involves proving equivalence between two designs, which may be at the same level or different levels of abstraction. Equivalence checking is often used to prove equivalence between the RTL model and the transistor-level schematic of the digital system. Equivalence checking in sequential circuits, i.e., digital circuits containing latches and flip-flops, typically consists of two steps. The first step involves constructing a latch mapping, also known as a register mapping. The latch mapping identifies corresponding latches in the two designs to be compared. Once the corresponding latches are identified, it is then possible to decompose the designs into corresponding combinational blocks. The second step is to verify whether the corresponding combinational blocks are equivalent. If the combinational blocks are equivalent, then the two designs are functionally equivalent.
There are various techniques for checking equivalence of combinational blocks. See, for example, Jerry R. Burch and Vigyan Singhal, xe2x80x9cRobust Latch Mapping for Combinational Equivalence Checking,xe2x80x9d Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, 1998, pages 563-569, Pranav Ashar et al., xe2x80x9cUsing Complete-1-Distinguishability for FSM Equivalence Checking,xe2x80x9d Proceedings of the 1996 IEEE/ACM International Conference on Computer-aided design, 1996, pages 346-353, and Andreas Kuehlmann and Florian Krohm, xe2x80x9cEquivalence Checking Using Cuts and Heaps,xe2x80x9d Proceedings of the 34th annual conference on Design automation conference, 1997, pages 263-268.
Various methods are known for constructing latch mapping between two designs. In general, these methods can be divided into three categories: structure mapping, function mapping, and name-matching mapping. Structure mapping involves matching structurally similar latches. For example, the latches 8, 10 shown in FIGS. 3A and 3B are structurally similar because they have their ports xe2x80x9cdxe2x80x9d connected to the same data block xe2x80x9cb1k.d[0],xe2x80x9d their ports xe2x80x9cqxe2x80x9d connected to the same net xe2x80x9c1063,xe2x80x9d and their ports xe2x80x9cclkxe2x80x9d connected to the same net xe2x80x9c2176.xe2x80x9d Thus, the latches 8, 10 will be correlated in the latch mapping. Function mapping involves analyzing and using the functional properties of the latches to correlate the designs. In function mapping, for example, two latches may be correlated because they have one set of ports connected to a net whose function is xe2x80x9caandbandcxe2x80x9d and another set of ports connected to a net whose function is xe2x80x9cclk.xe2x80x9d Name-matching mapping depends on the latches in the two design models having similar labels. For example, the labels xe2x80x9cX1xe2x80x9d and xe2x80x9cSX1xe2x80x9d of the latches 12, 14 shown in FIGS. 4A and 4B are similar because they both contain xe2x80x9cX1.xe2x80x9d Thus, the latches 12, 14 will be correlated in the latch mapping. Typically, there will be mapping rules that indicate which portions of the labels are relevant to latch mapping.
In the practical implementation of formal equivalence, label correspondence can become a weak link. This is because the circuit designer often uses different labels than the logic designer. Also, tools that perform design transformation, such as synthesis or clock tree insertion, often do not preserve labels, especially when the design is being flattened as part of the transformation. Thus, there is a possibility that some latches will be unmapped because they cannot be correlated to other latches. Thus, if two combinational blocks are found to not be equivalent, it may be because of an incorrect label matching rather than a bug in the circuit. This, of course, complicates the debugging process. However, in an environment with a naming convention, it is worthwhile to have a tool that can perform name matching mapping because the function/structure mapping techniques use complex algorithms that can sometimes fail. Also, function/structure mapping techniques are more suited to an environment where equivalence checking is being performed between two designs at the same level (e.g., gate-gate).
In one aspect, the invention is a method for constructing a latch mapping between a first level description and a second level description of a digital system, wherein the first level description and the second level descriptions identify components in the digital system using a predefined naming convention. The method comprises identifying first latch components in the first level description and, for each identified latch component, storing a first string comprising a selected property of the first latch component in a first storage. The method further includes identifying second latch components in the second level description and, for each identified second latch component, storing a second string comprising a selected property of the second latch component in a second storage. The method further includes generating a latch mapping by matching the first strings in the first storage with the second strings in the second storage.
Other aspects and advantages of the invention will be apparent from the following description and the appended claims.